*****∧I LISTINDUCTION1;

15 (∀v w.rev1(qNIL*v,w)=rev1(v,rev1(qNIL,w))∧∀uu.(∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w))⊃∀v w.rev1(uu*v,w)%
=rev1(v,rev1(uu,w))))⊃∀u v w.rev1(u*v,w)=rev1(v,rev1(u,w))  

*****EVAL ∀v w.rev1(qNIL*v,w)=rev1(v,rev1(qNIL,w)) BY { APPEND_DEF,REV1_DEF};

16 ∀v w.rev1(qNIL*v,w)=rev1(v,rev1(qNIL,w))  

*****ASSUME ∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w));

17 ∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w))  (17)

*****∀E APPEND_DEF uu,v;

18 (uu*v)=IF NULL uu THEN v ELSE cons(car uu,cdr uu*v)  

*****REWRITE ↑ BY LOGICTREE∪SEXPSS;

19 (uu*v)=cons(car uu,cdr uu*v)  

*****REWRITE rev1(uu*v,w) BY { 19};

20 rev1(uu*v,w)=rev1(cons(car uu,cdr uu*v),w)  

*****∀E REV1_DEF cons(car uu,cdr uu*v),w;

21 rev1(cons(car uu,cdr uu*v),w)=IF NULL cons(car uu,cdr uu*v) THEN w ELSE rev1(cdr cons(car uu,cdr uu*v),cons(c%
ar cons(car uu,cdr uu*v),w))  

*****REWRITE ↑ BY LOGICTREE∪SEXPSS;

22 rev1(cons(car uu,cdr uu*v),w)=rev1(cdr uu*v,cons(car uu,w))  

*****REWRITE ↑↑↑ BY { 22};

23 rev1(uu*v,w)=rev1(cdr uu*v,cons(car uu,w))  

*****∀I ↑ uu;

24 ∀uu.rev1(uu*v,w)=rev1(cdr uu*v,cons(car uu,w))  

*****REWRITE ↑↑ BY { H_DIS};

25 rev1(uu*v,w)=rev1(v,rev1(cdr uu,cons(car uu,w)))  (17)

*****∀E REV1_DEF uu,w;

26 rev1(uu,w)=IF NULL uu THEN w ELSE rev1(cdr uu,cons(car uu,w))  

*****REWRITE ↑ BY SEXPSS∪LOGICTREE;

27 rev1(uu,w)=rev1(cdr uu,cons(car uu,w))  

*****TAUTEQ rev1(cdr uu,cons(car uu,w))=rev1(uu,w) 27;

28 rev1(cdr uu,cons(car uu,w))=rev1(uu,w)  

*****REWRITE 25 BY { 28};

29 rev1(uu*v,w)=rev1(v,rev1(uu,w))  (17)

*****∀I ↑ v w;

30 ∀v w.rev1(uu*v,w)=rev1(v,rev1(uu,w))  (17)

*****⊃I H_DIS⊃↑;

31 ∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w))⊃∀v w.rev1(uu*v,w)=rev1(v,rev1(uu,w))  

*****∀I ↑ uu;

32 ∀uu.(∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w))⊃∀v w.rev1(uu*v,w)=rev1(v,rev1(uu,w)))  

*****TAUT ∀u v w.rev1(u*v,w)=rev1(v,rev1(u,w)) I_DIS:NIL_DIS,32;

33 ∀u v w.rev1(u*v,w)=rev1(v,rev1(u,w))